1. Field of the Invention
The present invention relates to systems and methods for verification of digital circuits.
2. Brief Description of the Related Art
The design of an integrated circuit may be broken down into several steps. In a first step, an overall architecture and behavior of an integrated circuit may be designed. Then, a specification of the design's high-level functionality is typically expressed at the register-transfer level (RTL) using a hardware description language (HDL). RTL description (also known as “register transfer logic”) is a description of an integrated circuit in terms of data flow between registers, which store information between clock cycles in the integrated circuit. The RTL description specifies what and where this information is stored and how it is passed through the integrated circuit during its operation.
After describing the design's high-level functionality, the functional design of the integrated circuit is implemented into gate level logic. Such implementation may be performed using, for example, logic synthesis electronic design automation (EDA) software. Then, the logical design of the integrated circuit is implemented into physical components representing transistors and their interconnecting wires. Such physical implementation may be performed, for example, using routing and placement EDA software. After the physical design of the integrated circuit is completed, the design is released for subsequent manufacture and production of the integrated circuit.
After each of the steps described above, verification is typically performed to ensure that the step was performed correctly. Generally, such verification involves testing the integrated circuit design over various combinations of input, internal, and process constraints.
Digital circuits such as processors or application specific integrated circuits (ASICS) have become increasingly complex over the last decades. Engineers developing, designing and testing digital circuits have to ensure that a digital circuit has the required functionality and that bugs or malfunctions are excluded as far as possible. The design of a digital circuit should thus be verified before the actual production starts to avoid costs for erroneous circuits having undetected bugs. Simulation of a digital circuit design was therefore frequently applied in order to simulate the function of a digital circuit design. Computing a simulation, however, can be time consuming and expensive with modern complex designs.
Formal verification of digital circuits has become an alternative or complementary tool to simulation of digital circuits. Verification of a digital circuit is usually performed during the design of a digital circuit to verify that the planned design provides the desired functionality without relevant bugs. Formal verification uses formal assertions or formal properties which describe aspects of behaviour of the digital circuit design. A set of the formal assertions or formal properties is used to describe the behaviour of functions of the digital circuit. The digital circuit is then verified by verifying that each one of the properties holds for the description of the digital circuit design. In many cases a design of a digital circuit is described at the register transfer level (RTL) using languages such as VHDL, Verilog, SystemVerilog, C, C++, System C or others.
It is important to know whether a design of a digital circuit has been completely verified or has been verified to an extent that verification can be considered sufficiently complete and safe. State of the art literature determines the coverage of a verification process by determining whether enough assertions or properties have been established to cover the entire behaviour of the design of the digital circuit. A summary of known methods is given in the article “Coverage Metrics for Formal Verification” by H. Chockler et al. Proceedings of CHARME, 2003. Additional methods have been disclosed, for example, in U.S. Patent Application Publication No. 2007/0226663, U.S. Pat. No. 6,484,134 and U.S. Pat. No. 8,359,561.
The patent application US 2006/0200789 A1 discloses a method for checking the connectivity of an integrated circuit mask layout against an electrical connection in a netlist. Such checks have been termed LVS (Layout versus Schematics) checks. The method is performed across the Internet based on a web browser using a secured connection.
The U.S. Pat. No. 6,363,478 B1 relates to a session processing module for a server adapted to communicate across the Internet with clients. The module identifies the client and established a connection upon identification, using compression and decryption parameters to be determined.
The U.S. Pat. No. 6,094,485 teaches a method for establishing an encrypted connection between a client and a server upon determining an available encryption strength for the connection.
With the advent of cloud computing, systems and methods have been proposed for running circuit verification in the cloud. With such systems, circuit design data, i.e. data pertaining to a design of a digital circuit, would be uploaded into the cloud to permit verification of the circuits. Such systems and methods suffer from security issues associated with transferring and storing circuit design data in the cloud.